(* # ===================================================================
   # Matrix Project
   # Copyright FEM-NUAA.CN 2020
   # =================================================================== *)

(** ** Matrix Module *)
Require Import Reals.
Open Scope R_scope.
Require Import Matrix.Mat.Mat_make.
Require Export Matrix.Mat.Matrix_Module.

Section Lemma_needed.
(* ################################################################# *)
(** * Definition of Some Lemmas *)

Lemma Rplus_assoc2 : forall a b c d ,(a+b)+(c+d) = (a+c)+(b+d).
Proof. intros. ring. Qed.

Lemma Rminus_assoc : forall x y z, x - y - z = x - (y + z).
Proof. intros. ring. Qed.

Lemma Rminus_assoc2 : forall x y z w,(x+y)-(z+w) = (x-z)+(y-w).
Proof. intros. ring. Qed.

Lemma Rminus_opp : forall x y , x - y = Ropp (y - x ).
Proof. intros. ring. Qed.

Lemma Rminus_self : forall x , x - x = 0.
Proof. intros. ring. Qed. 

Lemma Rmult_distr_l : forall x y z, (x+y)*z = x*z + y*z.
Proof. intros. ring. Qed.

Lemma Rmult_distr_r : forall x y z, x*(y+z) = x*y + x *z. 
Proof. intros. ring. Qed.

Lemma Rmult_add_distr_l : forall x y z, (x+y)*z = x*z + y*z.
Proof. intros. ring. Qed.

Lemma Rmult_add_distr_r : forall x y z, x*(y+z) = x*y + x *z. 
Proof. intros. ring. Qed.

Lemma Rmult_sub_distr_l : forall x y z, (x-y)*z = x*z - y*z.
Proof. intros. ring. Qed.

Lemma Rmult_sub_distr_r : forall x y z, x*(y-z) = x*y - x *z. 
Proof. intros. ring. Qed.

End Lemma_needed.
(** * Definition of Real Module *)

Module RM.

Definition A := R.
Definition One := 1.
Definition Zero := 0.

Definition opp := Ropp.
Definition add := Rplus.
Definition sub := Rminus.
Definition mul := Rmult.

Definition add_comm := Rplus_comm.
Definition add_assoc := Rplus_assoc.
Definition add_assoc2:= Rplus_assoc2.
Definition add_zero_l:= Rplus_0_l.
Definition add_zero_r := Rplus_0_r.

Definition sub_assoc := Rminus_assoc.
Definition sub_assoc2:= Rminus_assoc2.
Definition sub_opp := Rminus_opp.
Definition sub_zero_l := Rminus_0_l.
Definition sub_zero_r := Rminus_0_r.
Definition sub_self := Rminus_self.

(*Definition mul_one_l := Rmult_1_l.*)
Definition mul_add_distr_l:= Rmult_add_distr_l.
Definition mul_add_distr_r := Rmult_add_distr_r.
Definition mul_sub_distr_l := Rmult_sub_distr_l.
Definition mul_sub_distr_r := Rmult_sub_distr_r.
Definition mul_assoc := Rmult_assoc.
Definition mul_zero_l := Rmult_0_l.
Definition mul_zero_r := Rmult_0_r.
Definition mul_one_l:= Rmult_1_l.
Definition mul_one_r:= Rmult_1_r.
Definition mul_comm := Rmult_comm.

End RM.

(** * Definition of Real Matrix Module *)

Module RMatrix := Matrix(RM).

Definition RMtrans := @RMatrix.Mtrans.
Arguments RMtrans {m} {n}.

Definition RMadd := @RMatrix.Madd.
Arguments RMadd {m} {n}.

Definition RMsub := @RMatrix.Msub.
Arguments RMsub {m} {n}.

Definition RMopp := @RMatrix.Mopp.
Arguments RMopp {m} {n}.

Definition RMmul := @RMatrix.Mmul.
Arguments RMmul {m} {n} {p}.

Definition RMmulc_l := @RMatrix.Mmulc_l.
Arguments RMmulc_l {m} {n}.

Definition RMmulc_r := @RMatrix.Mmulc_r.
Arguments RMmulc_r {m} {n}.

Definition RMO := @RMatrix.MO.

Definition RMI := @RMatrix.MI.

Notation "m1 RM+ m2" := (RMadd m1 m2) (at level 65).

Notation "m1 RM- m2" := (RMsub m1 m2) (at level 65).

Notation " RM- m" := (RMopp m) (at level 65).

Notation "m1 RM* m2" := (RMmul m1 m2) (at level 60).

Notation "c RC* m" := (RMmulc_l c m) (at level 60).

Notation "m *RC c" := (RMmulc_r m c) (at level 60).

(*Definition RMeq_visit := @RMatrix.Meq_visit.
Arguments RMeq_visit {m} {n}. *)

Definition RMadd_comm := @RMatrix.Madd_comm.
Arguments RMadd_comm {m} {n}.

Definition RMadd_assoc := @RMatrix.Madd_assoc.
Arguments RMadd_assoc {m} {n}.

Definition RMadd_zero_l := @RMatrix.Madd_zero_l.
Arguments RMadd_zero_l {m} {n}.

Definition RMadd_zero_r := @RMatrix.Madd_zero_r.
Arguments RMadd_zero_r {m} {n}.

Definition RMsub_comm := @RMatrix.Msub_comm.
Arguments RMsub_comm {m} {n}.

Definition RMsub_assoc := @RMatrix.Msub_assoc.
Arguments RMsub_assoc {m} {n}.

Definition RMsub_O_l := @RMatrix.Msub_O_l.
Arguments RMsub_O_l {m} {n}.

Definition RMsub_O_r := @RMatrix.Msub_O_r.
Arguments RMsub_O_r {m} {n}.

Definition RMsub_self := @RMatrix.Msub_self.
Arguments RMsub_self {m} {n}.

Definition RMmul_distr := @RMatrix.Mmul_add_distr_l.
Arguments RMmul_distr {m} {n}.

Definition RMmul_assoc:= @RMatrix.Mmul_assoc.
Arguments RMmul_assoc {m} {n} {p} {k}.

Definition RMmul_zero_l:=@RMatrix.Mmul_zero_l.
Arguments RMmul_zero_l {m} {n}.

Definition RMmul_zero_r:=@RMatrix.Mmul_zero_r.
Arguments RMmul_zero_r {m}{n}.

Definition RMmul_mul_unit_l := @RMatrix.Mmul_unit_l.
Arguments RMmul_mul_unit_l {m} {n}.

Definition RMmul_mul_unit_r := @RMatrix.Mmul_unit_r.
Arguments RMmul_mul_unit_r {m} {n}.

Definition RMmulc_comm := @RMatrix.Mmulc_comm.
Arguments RMmulc_comm {m} {n}.

Definition RMmulc_distr_l :=@RMatrix.Mmulc_distr_l.
Arguments RMmulc_distr_l {m} {n}.

Definition RMmulc_0_l:=@RMatrix.Mmulc_0_l.
Arguments RMmulc_0_l {m} {n}.

Definition RMtteq := @RMatrix.Mtteq.
Arguments RMtteq {m} {n}.

Definition RMcteq := @RMatrix.Mcteq.
Arguments RMcteq {m} {n}.

Definition RMteq_add := @RMatrix.Mteq_add.
Arguments RMteq_add {m} {n}.

Definition RMteq_sub := @RMatrix.Mteq_sub.
Arguments RMteq_sub {m} {n}.

Definition RMteq_mul := @RMatrix.Mteq_mul.
Arguments RMteq_mul {m} {n}.

Definition RMtrans_MI:= @RMatrix.Mtrans_MI.
Arguments RMtrans_MI {n}.

Require Export Setoid.
Require Export Relation_Definitions.
Set Implicit Arguments.

Add Parametric Relation {m n:nat} : (Mat R m n) (@M_eq R m n) 
  reflexivity proved by (@Meq_ref R m n)
  symmetry proved by (@Meq_sym R m n)
  transitivity proved by (@Meq_trans R m n)
  as RMeq_rel.


Lemma Rmat_add_compat : 
  forall m n, 
     forall x x' : (Mat R m n ), @M_eq R m n x x' ->
     forall y y' : (Mat R m n ), @M_eq R m n y y'->
        @M_eq R m n (RMadd x y) (RMadd x' y').
Proof.
  intros.
  unfold RMadd,RMatrix.Madd. rewrite H,H0.
  reflexivity.
Qed.

Add Parametric Morphism {m n :nat}:(@RMadd m n)
  with signature (@M_eq R m n) ==> (@M_eq R m n) ==> (@M_eq R m n) 
  as Rmat_add_mor.
Proof.
exact (@Rmat_add_compat m n).
Qed.

Lemma Rmat_sub_compat : 
  forall m n, 
     forall x x' : (Mat R m n ), @M_eq R m n x x' ->
     forall y y' : (Mat R m n ), @M_eq R m n y y'->
        @M_eq R m n (RMsub x y) (RMsub x' y').
Proof.
  intros.
  unfold RMsub,RMatrix.Msub. rewrite H,H0.
  reflexivity.
Qed.

Add Parametric Morphism {m n :nat}:(@RMsub m n)
  with signature (@M_eq R m n) ==> (@M_eq R m n) ==> (@M_eq R m n) 
  as Rmat_sub_mor.
Proof.
exact (@Rmat_sub_compat m n).
Qed.

Lemma Rmat_opp_compat : 
  forall m n, 
     forall x x' : (Mat R m n ), @M_eq R m n x x' ->
        @M_eq R m n (RMopp x ) (RMopp x' ).
Proof.
  intros.
  unfold RMopp,RMatrix.Mopp. rewrite H.
  reflexivity.
Qed.

Add Parametric Morphism {m n :nat}:(@RMopp m n)
  with signature (@M_eq R m n) ==> (@M_eq R m n)
  as Rmat_opp_mor.
Proof.
exact (@Rmat_opp_compat m n).
Qed.

Lemma Rmat_trans_compat : 
  forall m n, 
     forall x x' : (Mat R m n ), @M_eq R m n x x' ->
        @M_eq R n m (RMtrans x ) (RMtrans x' ).
Proof.
  intros.
  unfold RMtrans,RMatrix.Mtrans. rewrite H.
  reflexivity.
Qed.

Add Parametric Morphism {m n :nat}:(@RMtrans m n)
  with signature (@M_eq R m n) ==> (@M_eq R n m)
  as Rmat_trans_mor.
Proof.
exact (@Rmat_trans_compat m n).
Qed.

Lemma Rmat_mul_compat : 
  forall m n p, 
     forall x x' : (Mat R m n ), @M_eq R m n x x' ->
     forall y y' : (Mat R n p ), @M_eq R n p y y'->
        @M_eq R m p (RMmul x y) (RMmul x' y').
Proof.
  intros.
  unfold RMmul,RMatrix.Mmul. rewrite H,H0.
  reflexivity.
Qed.

Add Parametric Morphism {m n p :nat}:(@RMmul m n p)
  with signature (@M_eq R m n) ==> (@M_eq R n p) ==> (@M_eq R m p) 
  as Rmat_mul_mor.
Proof.
exact (@Rmat_mul_compat m n p).
Qed.

Section test.


Definition tm1 := mkMat_2_2 1 2 3 4.

Definition tm2 := mkMat_2_2 3 4 5 6.

(* Compute( RMadd tm1 tm2). *)

End test.


